feat: add DeepThunk #41
Conversation
Reviewing code you don't understand can be a bit intimidating, but nonetheless having you look over it is very valuable! |
Equilibris
force-pushed
the
add-notion-of-a-deep-thunk
branch
from
c742a6b
to
da2df62
Compare
|
Fixed the comments, feel free to take a look when you have time @alexkeizer |
| /-! | ||
| # DeepThunk | ||
|
|
||
| `DeepThunk` corresponds approximately to the [trace](https://ncatlab.org/nlab/show/traced+monoidal+category) of a given polynomial functor. |
There was a problem hiding this comment.
I'm not sure if adding a link to ncatlab make the code more approachable (it's good to have references!) or less (people tend to be intimidated by ncat 🤣). Thanks for adding it, though, I guess ncat is the canonical source for categorical nonsense
DeepThunkcorresponds to the (co-)trace of a given polynomial functor, here we add the natural transformation required to generate them. These will later be used to inject into when generating syntax forcodefsyntax.This commit simply adds the code without using it.